FDL - Step of Proof: inv_image_ind

Step of Proof: inv_image_ind_a

9,38

Inference at * 1 1 1
Iof proof for Lemma inv image ind a:

1. T : Type
2. r : T

3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)
8. S
9. x : T

y:S. (f(y) = x)

P(y)

by (% Do induction on T using hyp 5 %
((((WFndHypInd 5 (-1))
(CollapseTHENM (RepD))

)

(CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
(C) inil_term)))

)

(C1:

(C1: 9. j : T
(C1: 10.

k:T. r(k,j)

(

y:S. (f(y) = k)

P(y))
(C1: 11. y : S
(C1: 12. f(y) = j
(C1:

P(y)
(C.

Definitions t T, x. t(x), x(s), P Q, x:A. B(x), x(s1,s2), , {T}, WellFnd{i}(A;x,y.R(x;y))